COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00007 00003	
C00008 ENDMK
C⊗;

			SOLUTIONS TO HW#3
			CS216  DEC 7,1976

I assume the facts, proved in class, that
(1) u*[v*w]=[u*v]*w and (1) u*NIL=u.
The following propositions correspond to the LISP definitions of the functions
which concern us here:
(2) u*v = if n u then v else a u.[[d u] * v]
(3) rev(u) = rev1(u,NIL)[Note: to save writing, I've renamed "reverse" to "rev"]
(4) rev1(u,v) = if n u then v else rev1(d u,a u . v)
(5) u % x = if n u then NIL else [[a u].x].[d u % x]
(6) u ⊗ v = if n v then NIL else [ u % a v] * [ u ⊗ d v ]

I wish to prove:  rev(u*v)=rev(v)*rev(u), rev(rev(u))=u, and u⊗[v*w]=[u⊗v]*[u⊗w]

First I prove a lemma,
(7) rev1(u,v)=rev(u)*v

Proof:  By induction on u.  The Induction hypothesis P(u) is ∀v.(rev1(u,v)=rev(u)*v)
Base case:  Assume u=NIL.  Then rev1(u,v) = if n u then v else rev1(d u,au .v)
= v = NIL*v =  rev1(NIL,NIL)*v = rev(u)*v
Induction step:  Assume ¬(n u) and that for all w, rev1(d u,w)=rev(d u)*w
Then rev1(u,v) = if n u then v else rev1(d u,a u . v) = rev1(d u, a u .v)
= rev(d u)*[a u . v] 		(by the induction hypothesis) 
= rev(d u)* [[a u . NIL] * v]   (by definition of * )
= [rev(d u) * [a u . NIL]] * v  (by 1)
= rev1[d u,a u . NIL] * v   	(by the induction hypothesis)
= rev1[u,NIL] * v	    	(by the definition of rev1)
= rev(u) * v		    	(by the definition of rev)

(8) rev(u*v)=rev(v)*rev(u)

Proof:  By induction on u.
Base case:  If u=NIL then rev(u*v) = rev(NIL*v) = rev(v) = rev(v) * NIL
= rev(v) * rev(NIL) = rev(v) * rev(u), since rev(NIL) = NIL (immediate from (3),(4))
Induction step:  Assume ¬(n u), and that for all w, rev(d u * w)=rev(w) * rev(d u)
Then rev(u*v) = rev1(u*v,NIL) = if n u*v then NIL else rev1(d [u*v],[a [u*v]].NIL)
Now u*v = if n u then v else a u.[[d u]*v] =a u.[[d u]*v] which is not NIL, thus
rev(u*v) = rev1(d [u*v],[a [u*v]].NIL) 
= rev(d [u*v])*[[a [u*v]]. NIL]		(by (7))
= rev(d [u*v]) * [a u . NIL]		(by definition of *) 
= rev([d u]*v) * [a u . NIL]		(by definition of *) 
= [rev(v)*rev(d u)]*[a u . NIL]  	(by induction hypothesis]
= rev(v)* [rev(d u)*[a u.NIL]]  	(by 1)
= rev(v) * [rev1(d u,a u . NIL)] 	(by 7)
= rev(v) * rev(u)			(by definition of rev,rev1)

(9) rev(rev(u))=u

Proof: By induction on u.
Base case: rev(rev(NIL))=NIL is immediate from the defintions of rev,rev1.
Induction step:  Assume ¬(n u) and rev(rev(d u))=d u.
Then rev(rev(u))=rev(rev1(u,NIL)) = rev(if n u then NIL else rev1(d u,a u . NIL))
= rev(rev1(d u,a u . NIL))
= rev(rev(d u)*[a u . NIL])  		(by 7)
= rev(a u .NIL) * rev(rev(d u))	 	(by 8)
= rev(a u . NIL) * d u			(by the induction hypothesis)
= [a u . NIL] * d u 			(by the definition of rev,rev1)
= u   				 	(by definition of *)



(10) u⊗[v*w]=[u⊗v]*[u⊗w]

Proof: By indution on v.
Base case: if v=NIL then u⊗[v*w]=u⊗[NIL*w]=u⊗w=NIL*[u⊗w]=[u⊗v]*[u⊗w]
Induction step: Assume ¬(n v) and u⊗[d v * w] = [u ⊗ d v] * [u ⊗ w]
Then u⊗[v*w] = if n v then NIL else [u % [a [v*w]]] * [u ⊗ d [v * w]]
= [u % [a [v*w]]] * [u ⊗ d [v *w]] 
= [u % [a v]]*[u ⊗ [[d v]*w]]		(by definition of *)
= [u % [a v]]*[[u ⊗ [d v]]*[u⊗w]] 	(by the induction hypothesis)
= [[u % [a v]] * [u ⊗ [d v]] ⊗ [u ⊗ w] 	(by 1)
= [u ⊗ v]*[u ⊗ w]    			(by definitition of ⊗)

Notice that in this last proof, we used no property of  the function % !